#include "util/usage.h"
#include "itpg/Solver.h"
#include "base/aig.h"
#include "cktsat/cktcover.h"
#include "cktsat/satsolver.h"
#include "util/util.h"
#include "itpg/qpf.h"


//      
//      Clause Operator
//
template<class cls_t >
class ClauseSaver : public SATSolver
{
   vec< cls_t > & c;
   public:
   ClauseSaver( vec< cls_t > & in ):c(in){}
   virtual ~ClauseSaver(){}
   virtual void addClause( vec<Lit> & x)
   {
      c.push();
      cls_t & y = c.last();
      y.growTo( x.size() );
      for( unsigned i = 0 ; i < x.size() ; ++i ) //TODO using copy here
         y[i] = x[i];
   }
};
//
//  mapping the lit with lut 
//
static plit_t mapping( plit_t in , plit_t * lut )
{
   plit_t x = lut[ var(in) ];
   return plit_t( var(x) , sign(x) ^ sign(in) );
}
//
//  shift the clause 
//
static void shift( const cls_t & x , cls_t & y , unsigned n )
{
   y.clear();
   y.growTo( x.size() );
   for( int i = 0 ; i < x.size() ; ++i )
      y[i] = plit_t( var(x[i]) + n , sign(x[i] ) );
}
// 
//  map the clause with lut 
//
static void mapping( cls_t & c , plit_t * lut )
{
   for( int i = 0 ; i < c.size() ; ++i )
      c[i] = mapping( c[i] , lut );
}
//
//  read circuit --> cnf --> solve 
//
template< class T >
static unsigned ckt2pf( T & ig , CktCover & ckt )
{
   vec< cls_t > cls;
   unsigned nvar;
   unsigned andFlag;
   AigLit   target;

   {
      ClauseSaver<cls_t> cs(cls);

      ckt.init(0); // no phase reducing  
      ckt.covering();
      ckt.assignLit(0);
      ckt.assignCNF( cs );

      nvar      = ckt.nVars();
      andFlag   = ckt._andFlag;
      target    = ckt._po[0];
   }

   ig.init( nvar+nvar);
   MinisatProof::Solver solver;
   solver.proof = new MinisatProof::Proof( ig ); // itp 
   plit_t lut[ nvar+nvar ];
   
   {// variable mapping 
      for( unsigned i = 0 ; i < nvar + nvar ; ++i )
         lut[i] = plit_t( i , 0 );
      for( unsigned i = 0 ; i < andFlag ; ++i )
      {
         unsigned v =  ckt._lits[i].var();
         lut[ v + nvar ] = plit_t( v , 0 );
      }
   }

   {// assign Lits 
      for( unsigned i = 0 ; i < nvar + nvar ; ++ i )
         solver.newVar();
   }

   {// assign Clause 
      cls_t c;
      {
         cls_t v;
         v.push( ckt._lits[var(target )] ^ sign(target) );
         
         shift( v , c , nvar );
         mapping( c , lut );
         c[0] = ~c[0];

         solver.addClause( v , 1);
         solver.addClause( c , 0); 
      }
      for( unsigned i = 0 ; i < cls.size() ; ++i )
      {
         shift( cls[i] , c , nvar );
         mapping( c , lut );

         solver.addClause( cls[i] , 1 );
         solver.addClause( c      , 0 );
      }
   }

   bool ret = solver.solve();
   if( ret == true ){ cout<< "error " << endl; exit(1);}
   //else { cout << "success" <<endl;}

   ig.done();
   ig.report();
   delete solver.proof;
   return nvar;
}
static AigLit mapping( AigLit in , AigLit * lut ){ return lut[var(in)] ^ sign(in) ;}
static AigLit build( const StrashAIG & in , StrashAIG & out , AigLit * lut )
{
   for( unsigned i = in._andFlag ; i < in.size() ; ++ i )
      lut[i] = out.createAND( mapping( in[i].fanin[0] , lut ) , mapping ( in[i].fanin[1] , lut )  );

   return mapping( in._po[0] , lut );
}
static void cir_quantifier( const StrashAIG & in , StrashAIG & out , vector<unsigned> & node , uint8_t forall ) 
{
   for( unsigned i = 1 ; i < in._andFlag ; ++i ) out.createBase();
   out._ppiFlag = out._andFlag = in._andFlag;

   AigLit o;
   if( forall ) o = toAigLit( 0 , 1 ); // forall -> and -> init 1
   else         o = toAigLit( 0 , 0 ); // exist --> or --> init 0

   unsigned lim = (1<<node.size());
   AigLit lut[ in.size() ];
   for( unsigned i = 0 ; i < in._andFlag ; ++i ) lut[i] = toAigLit( i , 0 );

   for( unsigned i = 0 ; i < lim ; ++ i )
   {
      for( unsigned j = 0 ; j < node.size() ; ++ j )
         if( i & (1<<j) ) 
            lut[ node[j] ] = toAigLit( 0 , 1 );
         else 
            lut[ node[j] ] = toAigLit( 0 , 0 );
      AigLit p = build( in , out , lut );
      if( forall ) o = out.createAND( o , p );
      else         o = inv( out.createAND( inv(o),inv(p) ) );
   }
   out._po.push( o );
}
static void cir_quantifier( const StrashAIG & in , StrashAIG & out , vector< std::pair<unsigned,uint8_t> > & qnode )
{
   vector<unsigned> n(1);
   const StrashAIG * before = & in ;
   bool init = true;

   assert( qnode.size() != 0 );

   while( qnode.size() )
   {
      std::pair<unsigned,uint8_t> q = qnode.back();
      qnode.pop_back();
      n[0] = q.first;
  
      StrashAIG * after_;
      if( qnode.size() )after_ = new StrashAIG;
      StrashAIG * after  = qnode.size()? ( after_ ) :( & out );

      cir_quantifier( *before , *after , n , (q.second%2)==0 );
      
      if( init )init=false;
      else      delete before;
      
      before = after;
   }
}
int main( unsigned argc , const char ** argv )
{
   ArgAnalyzer arg("qitp <file:aig> [-seed <int:seed>] [-n <int:node>] [-itp] [-duplication]" ,argc , argv );
   Usage usg;

   cout << "case : " << arg[0] << endl;
   unsigned seed = time(0);
   if( arg["-seed"].setted ) seed = atoi( arg["-seed"][0] );
   srand( seed );

   unsigned n = 3;
   if( arg["-n"].setted ) n = atoi( arg["-n"][0] );

   CktCover ckt;
   ckt.read_aig( arg[0].c_str() );
   if( n > (ckt._andFlag -1 ) ) return 1 ;

   // select the varialbe 
   // 0 is forall , 1 is exist , even is forall , odd is exist 
   vector< std::pair<unsigned,uint8_t> > qnode , qvar;
   {
      vector<unsigned> pis;
      for( unsigned i = 1 ; i < ckt._andFlag ; ++ i ) pis.push_back( i );
      random_shuffle( pis.begin() , pis.end() );
      
      for( unsigned i = 0 ; i < n ; ++ i ) 
         qnode.push_back( make_pair( pis[i] , n-i ) );
   }

   // duplication mode
   if( arg["-duplication"].setted )
   {
      StrashAIG nckt;
      cir_quantifier( ckt , nckt , qnode );
      
      nckt.write_aig( "qpf_d.aig" );
      nckt.report();
      usg.report();
      return 0;
   }


   QProof qpf;
   unsigned nvar = ckt2pf(  qpf , ckt );
   qvar = qnode; 
   for( unsigned i = 0 ; i < qnode.size() ; ++ i )
      qvar[i].first = ckt._lits[ qnode[i].first ].var() ;

   for( unsigned i = 0 ; i < qvar.size() ; ++ i)
      qpf.set_lvl( qvar[i].first , qvar[i].second );
   
   //qpf.swap_cls_by_iterate();
   qpf.swap_cls_by_propagate();

   qpf.check_resolve();
   qpf.check_connect();
   qpf.check_inorder();
   qpf.report();

   // dump the resoult
   if( arg["-itp"].setted )
   {
      StrashAIG nckt;
      for( unsigned i = 1 ; i < ckt._andFlag ; ++ i ) nckt.createBase();
      nckt._andFlag = nckt._ppiFlag = ckt._andFlag;
      int base[ nvar + nvar ];
      for( unsigned i = 0 ; i < nvar ; ++i ) base[i] = -1; // -1 or   exist
      for( unsigned i = nvar; i<nvar+nvar;++i)base[i]= -2; // -2 and  forall 
      for( unsigned i = 0 ; i < ckt._andFlag ; ++ i )base[ ckt._lits[i].var() ] = i;
      for( unsigned i = 0 ; i < qvar.size() ; ++ i  )
      {
         assert( qvar[i].second != 0 );
         base[ qvar[i].first ] = (((qvar[i].second%2)==0)?-2:-1);
      }
   
      qpf.interpolant( nckt , base);
      
      nckt.write_aig( "qpf_p.aig" );
      nckt.report();
      usg.report();
   }

   return 0;
}
//qpf.plot( "qpf.dot" );
//system( "dot -Tpng -O qpf.dot ; mv qpf.dot.png ~/public_html/");
